Cartesian Cubical Type Theory